/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package drt;

import java.util.Map;
import logic.Type;

/**
 *
 * @author phong
 */
public class DRSNegatedCondition extends DRSUnaryComplexCondition {
    
    public DRSNegatedCondition(DrtExpression term) {
        super(term);
        
        if (!term.getType().matches(Type.TRUTH_TYPE))
            throw new Error("incorrect type");
    }
    
    @Override
    public Type getType() {
        return Type.TRUTH_TYPE;
    }
    
    /*
     * we do not solve the double negated DRS
     * (it is not true that -(-DRS) = DRS
     */
    @Override
    public DRSNegatedCondition simplify() {
        return new DRSNegatedCondition(this.term.simplify());
    }
    
    @Override
    public DRSNegatedCondition replace(DrtVariable var, DrtExpression exp) {
        return new DRSNegatedCondition(this.term.replace(var, exp));
    }
    
    @Override
    public String toString() {
        return "-" + this.term.toString();
    }
    
    @Override
    public boolean equals(Object other) {
        if (other instanceof DRSNegatedCondition) {
            return this.term.equals(((DRSNegatedCondition)other).term);
        }
        return false;
    }    

    @Override
    public DRSNegatedCondition getTemplate(Map<String,String> map) {
        DrtExpression newTerm = this.term.getTemplate(map);
        return new DRSNegatedCondition(newTerm);
    }
}
